perm filename FRED.KRK[1,JRA] blob sn#026659 filedate 1973-02-23 generic text, type T, neo UTF8
00100	VAR:x,y,z,s;
00120	PRE_OP:cup,tbl,tat,thd,any,letgo, go ,pu,0,s0,fork;
00160	INF_PRED:=; EQUALITY: =;
00170	INF_OP:∩,∪;
00180	
00400	((x ∪ y)∩ z = 0) ⊃((x ∩ z) = 0 ∧ (y ∩ z = 0));
00500	FRED:
00550	tat(x,go(x,s))=tat(x,s) ∪ thd(s);
00600	thd(pu(go(x,s)))=any(tat(x,go(x,s)));
00700	thd(letgo(s))=0;
00800	 any(tat(cup,s0))∩fork=0;
00850	THEOREM:∃s¬ tat(tbl,s)∩ fork =0;
00900	;